perm filename KK.PRF[S79,JMC] blob
sn#437476 filedate 1979-04-26 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00002 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002
C00020 ENDMK
C⊗;
*****ASSUME A(RW,w,SP,0)∧k=K(w);
1 A(RW,w,SP,0)∧k=K(w) (1)
*****∧E ↑:#1;
2 A(RW,w,SP,0) (1)
*****∧E ↑↑:#2;
3 k=K(w) (1)
*****ASSUME Qs(k);
4 Qs(k) (4)
*****∀E QS k;
5 Qs(k)≡(OK(k)∧∃k1.(OK(k1)∧(s(k)=s(k1)∧¬(k=k1))))
*****TAUT OK(k) 4:5;
6 OK(k) (4)
*****TAUT ∃k1.(OK(k1)∧(s(k)=s(k1)∧¬(k=k1))) 4:5;
7 ∃k1.(OK(k1)∧(s(k)=s(k1)∧¬(k=k1))) (4)
*****∃E ↑ k1;
8 OK(k1)∧(s(k)=s(k1)∧¬(k=k1)) (8)
*****TAUTEQ A(RW,w,SP,0)∧(OK(k1)∧s(k)=s(k1)) 2,8;
9 A(RW,w,SP,0)∧(OK(k1)∧s(k)=s(k1)) (1 8)
*****SUBST 3 IN ↑;
10 A(RW,w,SP,0)∧(OK(k1)∧s(K(w))=s(k1)) (1 8)
*****∀E INIT3 w,k1;
11 (A(RW,w,SP,0)∧(OK(k1)∧s(K(w))=s(k1)))⊃∃w1.(A(w,w1,S,0)∧k1=K(w1))
*****⊃E ↑↑,↑;
12 ∃w1.(A(w,w1,S,0)∧k1=K(w1)) (1 8)
*****∃E ↑ w1;
13 A(w,w1,S,0)∧k1=K(w1) (13)
*****TAUTEQ A(w,w1,S,0)∧¬(K(w)=K(w1)) 3,8,13;
14 A(w,w1,S,0)∧¬(K(w)=K(w1)) (1 8 13)
*****∃I ↑ w1 ;
15 ∃w1.(A(w,w1,S,0)∧¬(K(w)=K(w1))) (1 4)
*****∀E BS w;
16 Bs(w)≡∃w1.(A(w,w1,S,0)∧¬(K(w)=K(w1)))
*****TAUT Bs(w) 15:16;
17 Bs(w) (1 4)
*****⊃I 4⊃↑;
18 Qs(k)⊃Bs(w) (1)
*****ASSUME Bs(w);
19 Bs(w) (19)
*****TAUT ∃w1.(A(w,w1,S,0)∧¬(K(w)=K(w1))) 16,19;
20 ∃w1.(A(w,w1,S,0)∧¬(K(w)=K(w1))) (19)
*****∃E ↑ w1;
21 A(w,w1,S,0)∧¬(K(w)=K(w1)) (21)
*****∀E OK w1;
22 OK(K(w1))
*****∀E INIT1 w,w1;
23 (A(RW,w,SP,0)∧A(w,w1,S,0))⊃s(K(w))=s(K(w1))
*****TAUTEQ s(K(w))=s(K(w1)) 2,21:23;
24 s(K(w))=s(K(w1)) (1 21)
*****SUBSTR 3 IN ↑;
25 s(k)=s(K(w1)) (1 21)
*****∧E 21:#2;
26 ¬(K(w)=K(w1)) (21)
*****SUBSTR 3 IN ↑;
27 ¬(k=K(w1)) (1 21)
*****∧I (22 (25 27));
28 OK(K(w1))∧(s(k)=s(K(w1))∧¬(k=K(w1))) (1 21)
*****∃I ↑ K(w1)←k1;
29 ∃k1.(OK(k1)∧(s(k)=s(k1)∧¬(k=k1))) (1 19)
*****∀E OK w;
30 OK(K(w))
*****SUBSTR 3 IN ↑;
31 OK(k) (1)
*****∧I (29 31);
32 ∃k1.(OK(k1)∧(s(k)=s(k1)∧¬(k=k1)))∧OK(k) (1 19)
*****TAUT Qs(k) 5,32;
33 Qs(k) (1 19)
*****⊃I 19⊃↑;
34 Bs(w)⊃Qs(k) (1)
*****≡I 18,↑;
35 Qs(k)≡Bs(w) (1)
*****⊃I 1⊃↑;
36 (A(RW,w,SP,0)∧k=K(w))⊃(Qs(k)≡Bs(w))
*****∀I ↑ w k;
37 ∀w k.((A(RW,w,SP,0)∧k=K(w))⊃(Qs(k)≡Bs(w)))
*****ASSUME Qp(k);
38 Qp(k) (38)
*****∀E QP k;
39 Qp(k)≡(OK(k)∧∃k1.(OK(k1)∧(p(k)=p(k1)∧¬(k=k1))))
*****TAUT OK(k) 38:39;
40 OK(k) (38)
*****TAUT ∃k1.(OK(k1)∧(p(k)=p(k1)∧¬(k=k1))) 38:39;
41 ∃k1.(OK(k1)∧(p(k)=p(k1)∧¬(k=k1))) (38)
*****∃E ↑ k1;
42 OK(k1)∧(p(k)=p(k1)∧¬(k=k1)) (42)
*****TAUTEQ A(RW,w,SP,0)∧(OK(k1)∧p(k)=p(k1)) 2,42;
43 A(RW,w,SP,0)∧(OK(k1)∧p(k)=p(k1)) (1 42)
*****SUBST 3 IN ↑;
44 A(RW,w,SP,0)∧(OK(k1)∧p(K(w))=p(k1)) (1 42)
*****∀E INIT4 w,k1;
45 (A(RW,w,SP,0)∧(OK(k1)∧p(K(w))=p(k1)))⊃∃w1.(A(w,w1,P,0)∧k1=K(w1))
*****⊃E ↑↑,↑;
46 ∃w1.(A(w,w1,P,0)∧k1=K(w1)) (1 42)
*****∃E ↑ w1;
47 A(w,w1,P,0)∧k1=K(w1) (47)
*****TAUTEQ A(w,w1,P,0)∧¬(K(w)=K(w1)) 3,42,47;
48 A(w,w1,P,0)∧¬(K(w)=K(w1)) (1 42 47)
*****∃I ↑ w1 ;
49 ∃w1.(A(w,w1,P,0)∧¬(K(w)=K(w1))) (1 38)
*****∀E BP w;
50 Bp(w)≡∃w1.(A(w,w1,P,0)∧¬(K(w)=K(w1)))
*****TAUT Bp(w) 49:50;
51 Bp(w) (1 38)
*****⊃I 38⊃↑;
52 Qp(k)⊃Bp(w) (1)
*****ASSUME Bp(w);
53 Bp(w) (53)
*****TAUT ∃w1.(A(w,w1,P,0)∧¬(K(w)=K(w1))) 50,53;
54 ∃w1.(A(w,w1,P,0)∧¬(K(w)=K(w1))) (53)
*****∃E ↑ w1;
55 A(w,w1,P,0)∧¬(K(w)=K(w1)) (55)
*****∀E INIT2 w,w1;
56 (A(RW,w,SP,0)∧A(w,w1,P,0))⊃p(K(w))=p(K(w1))
*****TAUTEQ p(K(w))=p(K(w1)) 2,55:56;
57 p(K(w))=p(K(w1)) (1 55)
*****∧E ↑↑↑:#2;
58 ¬(K(w)=K(w1)) (55)
*****∧I ((22 (57 58)));
59 OK(K(w1))∧(p(K(w))=p(K(w1))∧¬(K(w)=K(w1))) (1 55)
*****SUBSTR 3 IN ↑;
60 OK(K(w1))∧(p(k)=p(K(w1))∧¬(k=K(w1))) (1 55)
*****∃I ↑ K(w1)←k1;
61 ∃k1.(OK(k1)∧(p(k)=p(k1)∧¬(k=k1))) (1 53)
*****∧I ((31 61));
62 OK(k)∧∃k1.(OK(k1)∧(p(k)=p(k1)∧¬(k=k1))) (1 53)
*****TAUT Qp(k) 39,62;
63 Qp(k) (1 53)
*****⊃I 53⊃↑;
64 Bp(w)⊃Qp(k) (1)
*****≡I 52,↑;
65 Qp(k)≡Bp(w) (1)
*****⊃I 1⊃↑;
66 (A(RW,w,SP,0)∧k=K(w))⊃(Qp(k)≡Bp(w))
*****∀I ↑ w k;
67 ∀w k.((A(RW,w,SP,0)∧k=K(w))⊃(Qp(k)≡Bp(w)))
*****ASSUME Q1(k);
68 Q1(k) (68)
*****ASSUME A(w,w1,S,0);
69 A(w,w1,S,0) (69)
*****TAUT s(K(w))=s(K(w1)) 2,23,69;
70 s(K(w))=s(K(w1)) (1 69)
*****SUBSTR 3 IN ↑;
71 s(k)=s(K(w1)) (1 69)
*****∀E Q1 k;
72 Q1(k)≡(OK(k)∧∀k1.((OK(k1)∧s(k)=s(k1))⊃Qp(k1)))
*****TAUT OK(k)∧∀k1.((OK(k1)∧s(k)=s(k1))⊃Qp(k1)) 68,72;
73 OK(k)∧∀k1.((OK(k1)∧s(k)=s(k1))⊃Qp(k1)) (68)
*****∧E ↑:#2;
74 ∀k1.((OK(k1)∧s(k)=s(k1))⊃Qp(k1)) (68)
*****∀E ↑ K(w1);
75 (OK(K(w1))∧s(k)=s(K(w1)))⊃Qp(K(w1)) (68)
*****TAUT Qp(K(w1)) 22,71,75;
76 Qp(K(w1)) (1 68 69)
*****∀E SP w,w1,0;
77 (A(w,w1,S,0)∨A(w,w1,P,0))⊃A(w,w1,SP,0)
*****∀E AT RW,w,w1,SP,0;
78 (A(RW,w,SP,0)∧A(w,w1,SP,0))⊃A(RW,w1,SP,0)
*****∀E 67 w1,K(w1);
79 (A(RW,w1,SP,0)∧K(w1)=K(w1))⊃(Qp(K(w1))≡Bp(w1))
*****TAUTEQ Bp(w1) 2,69,76:79;
80 Bp(w1) (1 68 69)
*****⊃I 69⊃↑;
81 A(w,w1,S,0)⊃Bp(w1) (1 68)
*****∀I ↑ w1;
82 ∀w1.(A(w,w1,S,0)⊃Bp(w1)) (1 68)
*****∀E B1 w;
83 B1(w)≡∀w1.(A(w,w1,S,0)⊃Bp(w1))
*****TAUT B1(w) 82:83;
84 B1(w) (1 68)
*****⊃I 68⊃↑;
85 Q1(k)⊃B1(w) (1)
*****ASSUME B1(w);
86 B1(w) (86)
*****ASSUME OK(k1)∧s(k)=s(k1);
87 OK(k1)∧s(k)=s(k1) (87)
*****∀E INIT3 w,k1;
88 (A(RW,w,SP,0)∧(OK(k1)∧s(K(w))=s(k1)))⊃∃w1.(A(w,w1,S,0)∧k1=K(w1))
*****SUBSTR 3 IN ↑;
89 (A(RW,w,SP,0)∧(OK(k1)∧s(k)=s(k1)))⊃∃w1.(A(w,w1,S,0)∧k1=K(w1)) (1)
*****TAUT ∃w1.(A(w,w1,S,0)∧k1=K(w1)) 2,87,89;
90 ∃w1.(A(w,w1,S,0)∧k1=K(w1)) (1 87)
*****∃E ↑ w1;
91 A(w,w1,S,0)∧k1=K(w1) (91)
*****TAUT ∀w1.(A(w,w1,S,0)⊃Bp(w1)) 83,86;
92 ∀w1.(A(w,w1,S,0)⊃Bp(w1)) (86)
*****∀E ↑ w1;
93 A(w,w1,S,0)⊃Bp(w1) (86)
*****TAUTEQ Qp(K(w1)) 2,77:79,91,93;
94 Qp(K(w1)) (1 86 91)
*****∧E 91:#2;
95 k1=K(w1) (91)
*****SUBSTR ↑ IN ↑↑;
96 Qp(k1) (1 86 87)
*****⊃I 87⊃↑;
97 (OK(k1)∧s(k)=s(k1))⊃Qp(k1) (1 86)
*****∀I ↑ k1;
98 ∀k1.((OK(k1)∧s(k)=s(k1))⊃Qp(k1)) (1 86)
*****TAUT Q1(k) 31,72,98;
99 Q1(k) (1 86)
*****⊃I 86⊃↑;
100 B1(w)⊃Q1(k) (1)
*****≡I 85,↑;
101 Q1(k)≡B1(w) (1)
*****⊃I 1⊃↑;
102 (A(RW,w,SP,0)∧k=K(w))⊃(Q1(k)≡B1(w))
*****∀I ↑ w k;
103 ∀w k.((A(RW,w,SP,0)∧k=K(w))⊃(Q1(k)≡B1(w)))
*****∀E R1 k;
104 R1(k)≡(Qs(k)∧Q1(k))
*****∀E C1 w;
105 C1(w)≡(Bs(w)∧B1(w))
*****TAUT R1(k)≡C1(w) 35,101,104:105;
106 R1(k)≡C1(w) (1)
*****⊃I 1⊃↑;
107 (A(RW,w,SP,0)∧k=K(w))⊃(R1(k)≡C1(w))
*****∀I ↑ w k;
108 ∀w k.((A(RW,w,SP,0)∧k=K(w))⊃(R1(k)≡C1(w)))
*****ASSUME C2(RW);
109 C2(RW) (109)
*****∀E C2 RW;
110 C2(RW)≡(C1(RW)∧B2(RW))
*****∀E AR RW,SP,0;
111 A(RW,RW,SP,0)
*****∀E 108 RW,k0;
112 (A(RW,RW,SP,0)∧k0=K(RW))⊃(R1(k0)≡C1(RW))
*****TAUT R1(k0) RW,109:112;
113 R1(k0) (109)
*****TAUT B2(RW) 109:110;
114 B2(RW) (109)
*****ASSUME R1(k)∧p(k0)=p(k);
115 R1(k)∧p(k0)=p(k) (115)
*****TAUT OK(k)∧p(k0)=p(k) 5,104,115;
116 OK(k)∧p(k0)=p(k) (115)
*****SUBST RW IN ↑;
117 OK(k)∧p(K(RW))=p(k) (115)
*****∀E INIT4 RW,k;
118 (A(RW,RW,SP,0)∧(OK(k)∧p(K(RW))=p(k)))⊃∃w1.(A(RW,w1,P,0)∧k=K(w1))
*****TAUT ∃w1.(A(RW,w1,P,0)∧k=K(w1)) 111,117:118;
119 ∃w1.(A(RW,w1,P,0)∧k=K(w1)) (115)
*****∃E ↑ w1;
120 A(RW,w1,P,0)∧k=K(w1) (120)
*****∀E 108 w1,k;
121 (A(RW,w1,SP,0)∧k=K(w1))⊃(R1(k)≡C1(w1))
*****∀E SP RW,w1,0;
122 (A(RW,w1,S,0)∨A(RW,w1,P,0))⊃A(RW,w1,SP,0)
*****TAUT C1(w1) 115,120:122;
123 C1(w1) (115 120)
*****∀E LP RW,w1;
124 A(RW,RW,SP,0)⊃(A(RW,w1,P,1)≡(A(RW,w1,P,0)∧C1(w1)))
*****TAUT A(RW,w1,P,1) 111,120,123:124;
125 A(RW,w1,P,1) (115 120)
*****∀E B2 RW;
126 B2(RW)≡∀w1.(A(RW,w1,P,1)⊃K(RW)=K(w1))
*****TAUT ∀w1.(A(RW,w1,P,1)⊃K(RW)=K(w1)) 114,126;
127 ∀w1.(A(RW,w1,P,1)⊃K(RW)=K(w1)) (109)
*****∀E ↑ w1;
128 A(RW,w1,P,1)⊃K(RW)=K(w1) (109)
*****TAUTEQ k0=k RW,120,125,128;
129 k0=k (109 115)
*****⊃I 115⊃↑;
130 (R1(k)∧p(k0)=p(k))⊃k0=k (109)
*****∀I ↑ k←k1;
131 ∀k1.((R1(k1)∧p(k0)=p(k1))⊃k0=k1) (109)
*****∀E Q2 k0;
132 Q2(k0)≡(OK(k0)∧∀k1.((R1(k1)∧p(k0)=p(k1))⊃k0=k1))
*****∀E OK RW;
133 OK(K(RW))
*****SUBSTR RW IN ↑;
134 OK(k0)
*****TAUT Q2(k0) 131:132,134;
135 Q2(k0) (109)
*****∧I (135 113);
136 Q2(k0)∧R1(k0) (109)
*****∀E R2 k0;
137 R2(k0)≡(R1(k0)∧Q2(k0))
*****TAUT R2(k0) 136:137;
138 R2(k0) (109)
*****⊃I 109⊃↑;
139 C2(RW)⊃R2(k0)
*****∀E C1 RW;
140 C1(RW)≡(Bs(RW)∧B1(RW))
*****∀E C2 RW;
141 C2(RW)≡(C1(RW)∧B2(RW))
*****TAUT R2(k0) PK,NSK,SKNPK,139:141;
142 R2(k0)
*****ASSUME R2(k);
143 R2(k) (143)
*****∀E R2 k;
144 R2(k)≡(R1(k)∧Q2(k))
*****TAUT R1(k) 143:144;
145 R1(k) (143)
*****TAUT Q2(k) 143:144;
146 Q2(k) (143)
*****TAUT C1(w) 106,145;
147 C1(w) (1 143)
*****ASSUME A(w,w1,P,1);
148 A(w,w1,P,1) (148)
*****∀E LP w,w1;
149 A(RW,w,SP,0)⊃(A(w,w1,P,1)≡(A(w,w1,P,0)∧C1(w1)))
*****TAUT C1(w1) 1,148:149;
150 C1(w1) (1 148)
*****TAUT A(w,w1,P,0) 1,148:149;
151 A(w,w1,P,0) (1 148)
*****TAUT p(K(w))=p(K(w1)) 2,56,151;
152 p(K(w))=p(K(w1)) (1 148)
*****∀E 108 w1,K(w1);
153 (A(RW,w1,SP,0)∧K(w1)=K(w1))⊃(R1(K(w1))≡C1(w1))
*****TAUTEQ R1(K(w1)) 1,77:78,150:151,153;
154 R1(K(w1)) (1 148)
*****∀E Q2 k;
155 Q2(k)≡(OK(k)∧∀k1.((R1(k1)∧p(k)=p(k1))⊃k=k1))
*****TAUT OK(k)∧∀k1.((R1(k1)∧p(k)=p(k1))⊃k=k1) 146,155;
156 OK(k)∧∀k1.((R1(k1)∧p(k)=p(k1))⊃k=k1) (143)
*****∧E ↑:#2;
157 ∀k1.((R1(k1)∧p(k)=p(k1))⊃k=k1) (143)
*****∀E ↑ K(w1);
158 (R1(K(w1))∧p(k)=p(K(w1)))⊃k=K(w1) (143)
*****SUBST 3 IN ↑;
159 (R1(K(w1))∧p(K(w))=p(K(w1)))⊃K(w)=K(w1) (1 143)
*****TAUTEQ K(w)=K(w1) 152,154,159;
160 K(w)=K(w1) (1 143 148)
*****⊃I 148⊃↑;
161 A(w,w1,P,1)⊃K(w)=K(w1) (1 143)
*****∀I ↑ w1;
162 ∀w1.(A(w,w1,P,1)⊃K(w)=K(w1)) (1 143)
*****∀E C2 w;
163 C2(w)≡(C1(w)∧B2(w))
*****∀E B2 w;
164 B2(w)≡∀w1.(A(w,w1,P,1)⊃K(w)=K(w1))
*****TAUT C2(w) 147,162:164;
165 C2(w) (1 143)
*****⊃I 143⊃↑;
166 R2(k)⊃C2(w) (1)
*****⊃I 1⊃↑;
167 (A(RW,w,SP,0)∧k=K(w))⊃(R2(k)⊃C2(w))
*****∀I ↑ w k;
168 ∀w k.((A(RW,w,SP,0)∧k=K(w))⊃(R2(k)⊃C2(w)))
*****ASSUME R2(k1)∧s(k0)=s(k1);
169 R2(k1)∧s(k0)=s(k1) (169)
*****∀E R2 k1;
170 R2(k1)≡(R1(k1)∧Q2(k1))
*****∀E Q2 k1;
171 Q2(k1)≡(OK(k1)∧∀k.((R1(k)∧p(k1)=p(k))⊃k1=k))
*****TAUT OK(k1)∧s(k0)=s(k1) 169:171;
172 OK(k1)∧s(k0)=s(k1) (169)
*****∀E INIT3 RW,k1;
173 (A(RW,RW,SP,0)∧(OK(k1)∧s(K(RW))=s(k1)))⊃∃w1.(A(RW,w1,S,0)∧k1=K(w1))
*****SUBST RW IN ↑↑;
174 OK(k1)∧s(K(RW))=s(k1) (169)
*****TAUT ∃w1.(A(RW,w1,S,0)∧k1=K(w1)) 111,173:174;
175 ∃w1.(A(RW,w1,S,0)∧k1=K(w1)) (169)
*****∃E ↑ w1;
176 A(RW,w1,S,0)∧k1=K(w1) (176)
*****∀E 168 w1,k1;
177 (A(RW,w1,SP,0)∧k1=K(w1))⊃(R2(k1)⊃C2(w1))
*****∀E LS RW,w1;
178 A(RW,RW,SP,0)⊃(A(RW,w1,S,2)≡(A(RW,w1,S,0)∧C2(w1)))
*****∀E SK w1;
179 A(RW,w1,S,2)⊃K(RW)=K(w1)
*****TAUTEQ k0=k1 RW,111,122,169,176:179;
180 k0=k1 (169)
*****⊃I 169⊃↑;
181 (R2(k1)∧s(k0)=s(k1))⊃k0=k1
*****∀I ↑ k1;
182 ∀k1.((R2(k1)∧s(k0)=s(k1))⊃k0=k1)
*****∀E Q3 k0;
183 Q3(k0)≡(OK(k0)∧∀k1.((R2(k1)∧s(k0)=s(k1))⊃k0=k1))
*****TAUT Q3(k0) 134,182:183;
184 Q3(k0)
*****∀E R3 k0;
185 R3(k0)≡(R2(k0)∧Q3(k0))
*****TAUT R3(k0) 142,184:185;
186 R3(k0)